#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include "klee_change_macros.h"
#include "klee_change_functions.h"
int lib(int x) {
  if(klee_change(0,1)){
      if (x == 0)
         return -1;
      if (x < 0)
         return -1;
      else
         return 1;
  }
  else{
      if (x <= 0)
         return -1;
      else
         return 1;
  }
}

int client(int x){
  if (x > 0) {
    return lib(x);
  }
  return x;
}

int main(int argc, char *argv[]) {
  int x= argv[1][0] - '0';
  return client(x);
}
